\begin{tabbing}
$M$.ef($k$,$x$,$s$,$v$)?$w$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=fpf{-}cap(1of(2of(2of(2of(2of($M$)))));product{-}deq(Knd;Id;KindDeq;IdDeq);$\langle$$k$$,\,$$x$$\rangle$;$\lambda$$s$,$v$. $w$)\+
\\[0ex]($s$
\\[0ex],$v$)
\-
\end{tabbing}